FDL - Nuprl Lemma : combine-antecedent-surjections

Nuprl Lemma : combine-antecedent-surjections

es:ES, A, B, P, Q:(E

).
(

e:E.

(A(e) & B(e)))

(

e:E.

(P(e) & Q(e)))

(

e:E. Dec(P(e)))

(

e:E. Dec(A(e)))

(

e:E. Dec(B(e)))

(

f:({e:E| A(e)}

{e:E| P(e)} ), g:({e:E| B(e)}

{e:E| Q(e)} ).

P

f

A

Q

g

B

(

h:{e:E| (A(e))

(B(e))}

{e:E| (P(e))

(Q(e))}

(

(

e.(P(e))

(Q(e))

h

e.(A(e))

(B(e))

(

& (

e:{e:E| (A(e))

(B(e))} . (A(e))

(h(e) = f(e)))

(

& (

e:{e:E| (A(e))

(B(e))} . (

(A(e)))

(h(e) = g(e))))))

Definitions Q f P, Q f P, A c B, A, {T}, P Q, P Q, True, if b then t else f fi , ff, tt, b, P Q, x:A. B(x), t T, P & Q, P Q, , x:A. B(x), Unit, , False, Dec(P),

Lemmas es-causl wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, bnot wf, bool wf, false wf, true wf, assert wf, iff wf, bfalse wf, btrue wf, event system wf, not wf, decidable wf, es-E wf, antecedent-surjection wf